As one means for realizing rapid development in an LSI design and embedded software design, an assertion-based design/verification method, which describes restrictions represented by temporal logic (LTL, PSL, etc.) formulas as assertions in a specification, and conducts a design or verification using them has received a lot of attention (for example, see “non-patent reference 1” below). In the assertion-based design, assertions are defined as properties for respective components of a system, these properties attached to components are embedded in a system, and a design is conducted while verifying whether or not properties of components are violated in design processes.
Since a design problem includes processes for creating an entirety by appropriately combining parts, it is required to verify properties which appear only when components are combined (for example, properties across components and those as a completed system as a whole). However, a means for obtaining these properties from individual component properties has never been provided. For this reason, a technique for combining properties and extracting a necessary part is demanded.
On the other hand, in a formal verification theory of software, a verification technique such as model verification using properties described using logic formulas represented by LTL (Linear Temporal Logic) formulas has been studied. For example, in model verification, LTL formulas are temporarily converted into state transition machines (automata), and it is verified whether or not properties described using LTL formulas by combining the state transition machines and a model to be verified (which is also described as a state transition machine) is approved.
Therefore, it is considered to practically implement a technique which combines properties or extracts a necessary part by applying a technique for manipulating state transition machines based on a technique for converting temporal logic formulas into state transition machines.
As for the LTL (Linear Temporal Logic) as one type of temporal logics, a technique for converting the LTL formulas into alternating automata as one type of automata has been established (for example, see “non-patent reference 2” below). Furthermore, a technique for converting alternating automata into linear temporal logic formulas has also been established (for example, see “non-patent reference 3” below).    Non-patent Reference 1: “Assertion-based design” Second Edition, written by Harry D. Forster, Adam C. Krolnik, and David J. Lacey, edited by Teruo Higashino, Kozo Okano, and Akio Nakata, Maruzen Shoten    Non-patent Reference 2: “An Automata-Theoretic Approach To Linear Temporal Logic”, MY Vardi—Logics for Concurrency: Structure Versus Automata, 1996, Springer-Verlag Inc.    Non-patent Reference 3: “Deeper Connections between LTL and Alternating Automata”, Pelanek, R. and Strejcek, J., Proc. of Conference on Implementation and Application of Automata (CIAA 2005)